1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
/*!
Keywords and special characters
*/

/// The set of special characters
pub const SPECIAL_CHARACTERS: &str = "\n\r\t :[](){}#\"\',;.λΠ";

/// An assignment
pub const ASSIGN: &str = "=";

/// A function type arrow
pub const FN_ARROW: &str = "->";

/// A mapping arrow
pub const MAP_ARROW: &str = "=>";

/// A let statement
pub const LET: &str = "#let";

/// An equality check
pub const ASSERT_EQ: &str = "#eq";

/// A head reduction statement
pub const HEAD: &str = "#head";

/// A beta reduction statement
pub const BETA: &str = "#beta";

/// An eta reduction statement
pub const ETA: &str = "#eta";

/// A beta-eta reduction statement
pub const BETA_ETA: &str = "#betaeta";

/// A lambda function
pub const LAMBDA: &str = "λ";

/// A simple lambda function
pub const SIMPLE_LAMBDA: &str = "#lambda";

/// A dependent function type
pub const PI: &str = "Π";

/// A simple dependent function type
pub const SIMPLE_PI: &str = "#pi";

/// The keyword for typing universes
pub const UNIVERSE: &str = "#U";

/// The keyword for a typing universe variable
pub const UNIVERSE_VAR: &str = "#uv";

/// The keyword for true
pub const TRUE: &str = "#true";

/// The keyword for false
pub const FALSE: &str = "#false";

/// The keyword for the type of boolean values
pub const BOOL: &str = "#bool";

/// The keyword for a "hole"
pub const HOLE: &str = "_";

/// Check whether a string *not beginning with `#`* is a keyword or number
#[inline]
pub fn is_keyword(input: &str) -> bool {
    input == ASSIGN
        || input == FN_ARROW
        || input == MAP_ARROW
        || input == HOLE
        || input
            .chars()
            .next()
            .map(|c| char::is_digit(c, 10))
            .unwrap_or(false)
}